H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 0.848 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ LR

mainModule List

((mapAccumL :: (b -> c -> (b,a)) -> b -> [c] -> (b,[a])) :: (b -> c -> (b,a)) -> b -> [c] -> (b,[a]))

module List where

import qualified Maybe
import qualified Prelude

mapAccumL :: (b -> c -> (b,a)) -> b -> [c] -> (b,[a])

mapAccumL

_ s []

(s,[])

mapAccumL

f s (x : xs)

(s'',y : ys)

where

(\(s',_) ->s') vv5

s''

(\(s'',_) ->s'') vv6

vv5

f s x

vv6

mapAccumL f s' xs

(\(_,y) ->y) vv5

(\(_,ys) ->ys) vv6

module Maybe where

import qualified List
import qualified Prelude

Lambda Reductions:
The following Lambda expression

\(_,y)→y

is transformed to

y0 (_,y) = y

The following Lambda expression

\(_,ys)→ys

is transformed to

ys0 (_,ys) = ys

The following Lambda expression

\(s'',_)→s''

is transformed to

s''0 (s'',_) = s''

The following Lambda expression

\(s',_)→s'

is transformed to

s'0 (s',_) = s'

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

mainModule List

((mapAccumL :: (c -> b -> (c,a)) -> c -> [b] -> (c,[a])) :: (c -> b -> (c,a)) -> c -> [b] -> (c,[a]))

module List where

import qualified Maybe
import qualified Prelude

mapAccumL :: (c -> b -> (c,a)) -> c -> [b] -> (c,[a])

mapAccumL

_ s []

(s,[])

mapAccumL

f s (x : xs)

(s'',y : ys)

where

s'0 vv5

s''

s''0 vv6

s''0

(s'',_)

s''

s'0

(s',_)

vv5

f s x

vv6

mapAccumL f s' xs

y0 vv5

(_,y)

ys0 vv6

ys0

(_,ys)

module Maybe where

import qualified List
import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

mainModule List

((mapAccumL :: (b -> a -> (b,c)) -> b -> [a] -> (b,[c])) :: (b -> a -> (b,c)) -> b -> [a] -> (b,[c]))

module List where

import qualified Maybe
import qualified Prelude

mapAccumL :: (b -> a -> (b,c)) -> b -> [a] -> (b,[c])

mapAccumL

vw s []

(s,[])

mapAccumL

f s (x : xs)

(s'',y : ys)

where

s'0 vv5

s''

s''0 vv6

s''0

(s'',vz)

s''

s'0

(s',wu)

vv5

f s x

vv6

mapAccumL f s' xs

y0 vv5

(vy,y)

ys0 vv6

ys0

(vx,ys)

module Maybe where

import qualified List
import qualified Prelude

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

mainModule List

((mapAccumL :: (b -> c -> (b,a)) -> b -> [c] -> (b,[a])) :: (b -> c -> (b,a)) -> b -> [c] -> (b,[a]))

module List where

import qualified Maybe
import qualified Prelude

mapAccumL :: (b -> c -> (b,a)) -> b -> [c] -> (b,[a])

mapAccumL

vw s []

(s,[])

mapAccumL

f s (x : xs)

(s'',y : ys)

where

s'0 vv5

s''

s''0 vv6

s''0

(s'',vz)

s''

s'0

(s',wu)

vv5

f s x

vv6

mapAccumL f s' xs

y0 vv5

(vy,y)

ys0 vv6

ys0

(vx,ys)

module Maybe where

import qualified List
import qualified Prelude

Let/Where Reductions:
The bindings of the following Let/Where expression

(s'',y : ys)

where

s' = s'0 vv5

s'' = s''0 vv6

s''0 (s'',vz) = s''

s'0 (s',wu) = s'

vv5 = f s x

vv6 = mapAccumL f s' xs

y = y0 vv5

y0 (vy,y) = y

ys = ys0 vv6

ys0 (vx,ys) = ys

are unpacked to the following functions on top level

mapAccumLYs wx wy wz xu = mapAccumLYs0 wx wy wz xu (mapAccumLVv6 wx wy wz xu)

mapAccumLYs0 wx wy wz xu (vx,ys) = ys

mapAccumLS''0 wx wy wz xu (s'',vz) = s''

mapAccumLVv5 wx wy wz xu = wx wy wz

mapAccumLS'' wx wy wz xu = mapAccumLS''0 wx wy wz xu (mapAccumLVv6 wx wy wz xu)

mapAccumLVv6 wx wy wz xu = mapAccumL wx (mapAccumLS' wx wy wz xu) xu

mapAccumLS'0 wx wy wz xu (s',wu) = s'

mapAccumLY wx wy wz xu = mapAccumLY0 wx wy wz xu (mapAccumLVv5 wx wy wz xu)

mapAccumLY0 wx wy wz xu (vy,y) = y

mapAccumLS' wx wy wz xu = mapAccumLS'0 wx wy wz xu (mapAccumLVv5 wx wy wz xu)

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ Narrow

mainModule List

(mapAccumL :: (c -> a -> (c,b)) -> c -> [a] -> (c,[b]))

module List where

import qualified Maybe
import qualified Prelude

mapAccumL :: (b -> a -> (b,c)) -> b -> [a] -> (b,[c])

mapAccumL	vw s []	=	(s,[])
mapAccumL	f s (x : xs)	=	(mapAccumLS'' f s x xs,mapAccumLY f s x xs : mapAccumLYs f s x xs)

mapAccumLS'

wx wy wz xu

mapAccumLS'0 wx wy wz xu (mapAccumLVv5 wx wy wz xu)

mapAccumLS''

wx wy wz xu

mapAccumLS''0 wx wy wz xu (mapAccumLVv6 wx wy wz xu)

mapAccumLS''0

wx wy wz xu (s'',vz)

s''

mapAccumLS'0

wx wy wz xu (s',wu)

mapAccumLVv5

wx wy wz xu

wx wy wz

mapAccumLVv6

wx wy wz xu

mapAccumL wx (mapAccumLS' wx wy wz xu) xu

mapAccumLY

wx wy wz xu

mapAccumLY0 wx wy wz xu (mapAccumLVv5 wx wy wz xu)

mapAccumLY0

wx wy wz xu (vy,y)

mapAccumLYs

wx wy wz xu

mapAccumLYs0 wx wy wz xu (mapAccumLVv6 wx wy wz xu)

mapAccumLYs0

wx wy wz xu (vx,ys)

module Maybe where

import qualified List
import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="mapAccumL",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="mapAccumL xv3",fontsize=16,color="grey",shape="box"];3 -> 4[label="",style="dashed", color="grey", weight=3];
4[label="mapAccumL xv3 xv4",fontsize=16,color="grey",shape="box"];4 -> 5[label="",style="dashed", color="grey", weight=3];
5[label="mapAccumL xv3 xv4 xv5",fontsize=16,color="burlywood",shape="triangle"];45[label="xv5/xv50 : xv51",fontsize=10,color="white",style="solid",shape="box"];5 -> 45[label="",style="solid", color="burlywood", weight=9];
45 -> 6[label="",style="solid", color="burlywood", weight=3];
46[label="xv5/[]",fontsize=10,color="white",style="solid",shape="box"];5 -> 46[label="",style="solid", color="burlywood", weight=9];
46 -> 7[label="",style="solid", color="burlywood", weight=3];
6[label="mapAccumL xv3 xv4 (xv50 : xv51)",fontsize=16,color="black",shape="box"];6 -> 8[label="",style="solid", color="black", weight=3];
7[label="mapAccumL xv3 xv4 []",fontsize=16,color="black",shape="box"];7 -> 9[label="",style="solid", color="black", weight=3];
8[label="(mapAccumLS'' xv3 xv4 xv50 xv51,mapAccumLY xv3 xv4 xv50 xv51 : mapAccumLYs xv3 xv4 xv50 xv51)",fontsize=16,color="green",shape="box"];8 -> 10[label="",style="dashed", color="green", weight=3];
8 -> 11[label="",style="dashed", color="green", weight=3];
8 -> 12[label="",style="dashed", color="green", weight=3];
9[label="(xv4,[])",fontsize=16,color="green",shape="box"];10[label="mapAccumLS'' xv3 xv4 xv50 xv51",fontsize=16,color="black",shape="box"];10 -> 13[label="",style="solid", color="black", weight=3];
11[label="mapAccumLY xv3 xv4 xv50 xv51",fontsize=16,color="black",shape="box"];11 -> 14[label="",style="solid", color="black", weight=3];
12[label="mapAccumLYs xv3 xv4 xv50 xv51",fontsize=16,color="black",shape="box"];12 -> 15[label="",style="solid", color="black", weight=3];
13 -> 19[label="",style="dashed", color="red", weight=0];
13[label="mapAccumLS''0 xv3 xv4 xv50 xv51 (mapAccumLVv6 xv3 xv4 xv50 xv51)",fontsize=16,color="magenta"];13 -> 20[label="",style="dashed", color="magenta", weight=3];
14 -> 24[label="",style="dashed", color="red", weight=0];
14[label="mapAccumLY0 xv3 xv4 xv50 xv51 (mapAccumLVv5 xv3 xv4 xv50 xv51)",fontsize=16,color="magenta"];14 -> 25[label="",style="dashed", color="magenta", weight=3];
15 -> 29[label="",style="dashed", color="red", weight=0];
15[label="mapAccumLYs0 xv3 xv4 xv50 xv51 (mapAccumLVv6 xv3 xv4 xv50 xv51)",fontsize=16,color="magenta"];15 -> 30[label="",style="dashed", color="magenta", weight=3];
20[label="mapAccumLVv6 xv3 xv4 xv50 xv51",fontsize=16,color="black",shape="triangle"];20 -> 22[label="",style="solid", color="black", weight=3];
19[label="mapAccumLS''0 xv3 xv4 xv50 xv51 xv6",fontsize=16,color="burlywood",shape="triangle"];50[label="xv6/(xv60,xv61)",fontsize=10,color="white",style="solid",shape="box"];19 -> 50[label="",style="solid", color="burlywood", weight=9];
50 -> 23[label="",style="solid", color="burlywood", weight=3];
25[label="mapAccumLVv5 xv3 xv4 xv50 xv51",fontsize=16,color="black",shape="triangle"];25 -> 27[label="",style="solid", color="black", weight=3];
24[label="mapAccumLY0 xv3 xv4 xv50 xv51 xv7",fontsize=16,color="burlywood",shape="triangle"];51[label="xv7/(xv70,xv71)",fontsize=10,color="white",style="solid",shape="box"];24 -> 51[label="",style="solid", color="burlywood", weight=9];
51 -> 28[label="",style="solid", color="burlywood", weight=3];
30 -> 20[label="",style="dashed", color="red", weight=0];
30[label="mapAccumLVv6 xv3 xv4 xv50 xv51",fontsize=16,color="magenta"];29[label="mapAccumLYs0 xv3 xv4 xv50 xv51 xv8",fontsize=16,color="burlywood",shape="triangle"];53[label="xv8/(xv80,xv81)",fontsize=10,color="white",style="solid",shape="box"];29 -> 53[label="",style="solid", color="burlywood", weight=9];
53 -> 32[label="",style="solid", color="burlywood", weight=3];
22 -> 5[label="",style="dashed", color="red", weight=0];
22[label="mapAccumL xv3 (mapAccumLS' xv3 xv4 xv50 xv51) xv51",fontsize=16,color="magenta"];22 -> 33[label="",style="dashed", color="magenta", weight=3];
22 -> 34[label="",style="dashed", color="magenta", weight=3];
23[label="mapAccumLS''0 xv3 xv4 xv50 xv51 (xv60,xv61)",fontsize=16,color="black",shape="box"];23 -> 35[label="",style="solid", color="black", weight=3];
27[label="xv3 xv4 xv50",fontsize=16,color="green",shape="box"];27 -> 36[label="",style="dashed", color="green", weight=3];
27 -> 37[label="",style="dashed", color="green", weight=3];
28[label="mapAccumLY0 xv3 xv4 xv50 xv51 (xv70,xv71)",fontsize=16,color="black",shape="box"];28 -> 38[label="",style="solid", color="black", weight=3];
32[label="mapAccumLYs0 xv3 xv4 xv50 xv51 (xv80,xv81)",fontsize=16,color="black",shape="box"];32 -> 39[label="",style="solid", color="black", weight=3];
33[label="xv51",fontsize=16,color="green",shape="box"];34[label="mapAccumLS' xv3 xv4 xv50 xv51",fontsize=16,color="black",shape="box"];34 -> 40[label="",style="solid", color="black", weight=3];
35[label="xv60",fontsize=16,color="green",shape="box"];36[label="xv4",fontsize=16,color="green",shape="box"];37[label="xv50",fontsize=16,color="green",shape="box"];38[label="xv71",fontsize=16,color="green",shape="box"];39[label="xv81",fontsize=16,color="green",shape="box"];40 -> 41[label="",style="dashed", color="red", weight=0];
40[label="mapAccumLS'0 xv3 xv4 xv50 xv51 (mapAccumLVv5 xv3 xv4 xv50 xv51)",fontsize=16,color="magenta"];40 -> 42[label="",style="dashed", color="magenta", weight=3];
42 -> 25[label="",style="dashed", color="red", weight=0];
42[label="mapAccumLVv5 xv3 xv4 xv50 xv51",fontsize=16,color="magenta"];41[label="mapAccumLS'0 xv3 xv4 xv50 xv51 xv9",fontsize=16,color="burlywood",shape="triangle"];57[label="xv9/(xv90,xv91)",fontsize=10,color="white",style="solid",shape="box"];41 -> 57[label="",style="solid", color="burlywood", weight=9];
57 -> 43[label="",style="solid", color="burlywood", weight=3];
43[label="mapAccumLS'0 xv3 xv4 xv50 xv51 (xv90,xv91)",fontsize=16,color="black",shape="box"];43 -> 44[label="",style="solid", color="black", weight=3];
44[label="xv90",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ QDP

                      ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_mapAccumLVv6(xv3, xv50, xv51, ba, bb, bc) → new_mapAccumL(xv3, xv51, ba, bb, bc)
new_mapAccumL(xv3, :(xv50, xv51), ba, bb, bc) → new_mapAccumLVv6(xv3, xv50, xv51, ba, bb, bc)
new_mapAccumL(xv3, :(xv50, xv51), ba, bb, bc) → new_mapAccumL(xv3, xv51, ba, bb, bc)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_mapAccumL(xv3, :(xv50, xv51), ba, bb, bc) → new_mapAccumLVv6(xv3, xv50, xv51, ba, bb, bc)
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3, 3 >= 4, 4 >= 5, 5 >= 6
new_mapAccumL(xv3, :(xv50, xv51), ba, bb, bc) → new_mapAccumL(xv3, xv51, ba, bb, bc)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3, 4 >= 4, 5 >= 5
new_mapAccumLVv6(xv3, xv50, xv51, ba, bb, bc) → new_mapAccumL(xv3, xv51, ba, bb, bc)
The graph contains the following edges 1 >= 1, 3 >= 2, 4 >= 3, 5 >= 4, 6 >= 5